(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 6.
The certificate found is represented by the following graph.
Start state: 554
Accept states: [555, 556, 557]
Transitions:
554→555[foo_1|0]
554→556[bar_1|0]
554→557[p_1|0]
554→554[0_1|0, s_1|0]
554→558[s_1|1]
554→567[s_1|1]
554→571[s_1|1]
554→575[s_1|1]
554→600[s_1|1]
554→560[s_1|2]
554→577[s_1|2]
554→604[s_1|2]
554→611[s_1|2]
554→581[bar_1|2]
554→613[s_1|2, s_1|3]
554→566[s_1|2]
554→617[bar_1|2, bar_1|3]
558→559[p_1|1]
559→560[s_1|1]
559→566[s_1|2]
560→561[s_1|1]
560→565[p_1|2]
561→562[s_1|1]
561→564[p_1|2]
562→563[p_1|1]
563→564[p_1|1]
564→565[p_1|1]
565→566[s_1|1]
566→555[0_1|1]
567→568[s_1|1]
568→569[s_1|1]
568→556[0_1|2]
568→581[0_1|2]
568→636[s_1|2]
568→645[s_1|3]
568→617[0_1|2]
568→638[s_1|2, s_1|3]
568→647[s_1|4]
568→644[s_1|3, s_1|2]
568→653[s_1|4]
569→570[p_1|1]
570→556[0_1|1]
570→581[0_1|1]
570→636[s_1|2]
570→617[0_1|1]
570→638[s_1|3]
570→644[s_1|3]
571→572[s_1|1]
572→573[s_1|1]
573→574[s_1|1]
574→557[0_1|1]
575→576[p_1|1]
576→577[s_1|1]
576→581[bar_1|2]
577→578[s_1|1]
577→580[p_1|2]
578→579[p_1|1]
579→580[p_1|1]
580→581[bar_1|1]
581→582[s_1|1]
581→584[s_1|2]
581→588[foo_1|2]
582→583[p_1|1]
583→584[s_1|1]
583→588[foo_1|2]
584→585[s_1|1]
584→587[p_1|2]
585→586[p_1|1]
586→587[p_1|1]
587→588[foo_1|1]
588→589[s_1|1]
588→591[s_1|2]
588→599[s_1|2]
589→590[p_1|1]
590→591[s_1|1]
590→599[s_1|2]
591→592[s_1|1]
591→594[s_1|2]
591→598[p_1|2]
592→593[p_1|1]
593→594[s_1|1]
593→598[p_1|2]
594→595[s_1|1]
594→597[p_1|2]
595→596[p_1|1]
596→597[p_1|1]
597→598[p_1|1]
598→599[s_1|1]
599→555[p_1|1]
600→601[s_1|1]
600→603[p_1|2]
601→602[p_1|1]
602→603[p_1|1]
603→604[s_1|1]
603→611[s_1|2]
603→613[s_1|3]
603→617[bar_1|3]
604→605[foo_1|1]
605→606[s_1|1]
605→610[s_1|2]
605→582[s_1|2]
605→584[s_1|2]
605→588[foo_1|2]
605→618[s_1|2]
605→620[s_1|2, s_1|3]
605→624[foo_1|2, foo_1|3]
606→607[s_1|1]
606→609[p_1|2]
607→608[p_1|1]
608→609[p_1|1]
609→610[s_1|1]
609→582[s_1|2]
609→584[s_1|2]
609→588[foo_1|2]
609→618[s_1|2]
609→620[s_1|2, s_1|3]
609→624[foo_1|2, foo_1|3]
610→556[p_1|1]
610→581[p_1|1]
610→617[p_1|1]
611→612[p_1|2]
612→613[s_1|2]
612→617[bar_1|3]
613→614[s_1|2]
613→616[p_1|3]
614→615[p_1|2]
615→616[p_1|2]
616→617[bar_1|2]
617→618[s_1|2]
617→620[s_1|3]
617→624[foo_1|3]
618→619[p_1|2]
619→620[s_1|2]
619→624[foo_1|3]
620→621[s_1|2]
620→623[p_1|3]
621→622[p_1|2]
622→623[p_1|2]
623→624[foo_1|2]
624→625[s_1|2]
624→627[s_1|3]
624→635[s_1|3]
624→606[s_1|3, s_1|2]
624→610[s_1|4, s_1|3, s_1|2]
624→582[s_1|3, s_1|2, s_1|4]
624→584[s_1|3, s_1|2, s_1|4]
624→588[foo_1|3, foo_1|2, foo_1|4]
624→618[s_1|2, s_1|3, s_1|4]
624→620[s_1|2, s_1|3, s_1|4]
624→624[foo_1|2, foo_1|3, foo_1|4]
625→626[p_1|2]
626→627[s_1|2]
626→635[s_1|3]
626→606[s_1|3, s_1|2]
626→610[s_1|3, s_1|2]
626→582[s_1|3, s_1|2]
626→584[s_1|3, s_1|2]
626→588[foo_1|3, foo_1|2]
626→618[s_1|2, s_1|3]
626→620[s_1|2, s_1|3]
626→624[foo_1|2, foo_1|3]
627→628[s_1|2]
627→630[s_1|3]
627→634[p_1|3]
628→629[p_1|2]
629→630[s_1|2]
629→634[p_1|3]
630→631[s_1|2]
630→633[p_1|3]
631→632[p_1|2]
632→633[p_1|2]
633→634[p_1|2]
634→635[s_1|2]
634→606[s_1|2]
634→610[s_1|3, s_1|2]
634→582[s_1|2, s_1|3]
634→584[s_1|2, s_1|3]
634→588[foo_1|2, foo_1|3]
634→618[s_1|2, s_1|3]
634→620[s_1|2, s_1|3]
634→624[foo_1|2, foo_1|3]
635→605[p_1|2]
636→637[p_1|2]
637→638[s_1|2]
637→644[s_1|3]
638→639[s_1|2]
638→643[p_1|3]
639→640[s_1|2]
639→642[p_1|3]
640→641[p_1|2]
641→642[p_1|2]
642→643[p_1|2]
643→644[s_1|2]
644→588[0_1|2]
644→624[0_1|2]
644→645[s_1|3]
644→647[s_1|4]
644→653[s_1|4]
645→646[p_1|3]
646→647[s_1|3]
646→653[s_1|4]
647→648[s_1|3]
647→652[p_1|4]
648→649[s_1|3]
648→651[p_1|4]
649→650[p_1|3]
650→651[p_1|3]
651→652[p_1|3]
652→653[s_1|3]
653→588[0_1|3]
653→624[0_1|3]
653→654[s_1|4]
653→645[s_1|3]
653→656[s_1|5]
653→647[s_1|4]
653→653[s_1|4]
653→662[s_1|5]
654→655[p_1|4]
655→656[s_1|4]
655→662[s_1|5]
656→657[s_1|4]
656→661[p_1|5]
657→658[s_1|4]
657→660[p_1|5]
658→659[p_1|4]
659→660[p_1|4]
660→661[p_1|4]
661→662[s_1|4]
662→588[0_1|4]
662→624[0_1|4]
662→654[s_1|4]
662→645[s_1|3]
662→678[s_1|5]
662→656[s_1|5]
662→647[s_1|4]
662→653[s_1|4]
662→680[s_1|6]
662→662[s_1|5]
662→686[s_1|6]
678→679[p_1|5]
679→680[s_1|5]
679→686[s_1|6]
680→681[s_1|5]
680→685[p_1|6]
681→682[s_1|5]
681→684[p_1|6]
682→683[p_1|5]
683→684[p_1|5]
684→685[p_1|5]
685→686[s_1|5]
686→588[0_1|5]
686→624[0_1|5]
686→654[s_1|4]
686→645[s_1|3]
686→678[s_1|5]
686→656[s_1|5]
686→647[s_1|4]
686→653[s_1|4]
686→680[s_1|6]
686→662[s_1|5]
686→686[s_1|6]